COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	COMMENT$ Here is a set of first order axioms for the integers based on
C00005 ENDMK
C⊗;
COMMENT$ Here is a set of first order axioms for the integers based on
the successor operation written SUCC and the predecessor operation
written PRED.  While the axioms don't mention sets, they are compatible
with a later imbedding into set theory, because the SORT mechanism of
FOL relativizes the axioms to the domain NATNUM, so other domains are
possible.  It is a blemish that the axioms for PLUS, TIMES, etc. are
given as axioms, because they are really just definitions.  Taking
these definitions as axioms means that when we make the definitions,
we are asserting that no contradictions are thereby introduced.  A proper
definition mechanism is conservative in that no new facts are introduced
by definitions.  These particular definitions introduce no new facts, but
this is not syntactically obvious.$


DECLARE INDVAR I I1 I2 I3 J J1 J2 J3
K K1 K2 K3 L L1 L2 L3
M M1 M2 M3 N N1 N2 N3
 ε NATNUM;
DECLARE OPCONST SUCC: NATNUM → NATNUM [PRE];
DECLARE OPCONST PRED: NATNUM → INTEGER [PRE];
DECLARE INDVAR X Y Z;
DECLARE PREDPAR P(NATNUM);


AXIOM PRED:	∀N.(¬N=0 ⊃ NATNUM(PRED N));;

AXIOM PEANO:	∀N.(¬SUCC N = 0),
		∀N.PRED SUCC N = N,
		∀N.(¬N=0 ⊃ SUCC PRED N = N);;

AXIOM INDUCTION:P(0) ∧ ∀N.(P(N) ⊃ P(SUCC N)) ⊃ ∀N.P(N);;


COMMENT$ The rest of these axioms are really just definitions.$

DECLARE OPCONST +(NATNUM,NATNUM)=NATNUM[R←475,L←470];
DECLARE PREDCONST ≥(NATNUM,NATNUM)[INF];
DECLARE OPCONST *(NATNUM,NATNUM)=NATNUM[R←555,L←550];
DECLARE OPCONST -(NATNUM,NATNUM)=INTEGER[R←455,L←450];

AXIOM PLUS:	∀M.(M+0=M),
		∀M N.(M+SUCC N =SUCC(M+N));;

AXIOM TIMES:	∀M. M*0=0,
		∀M.M*1=M,
		∀M N. M*SUCC N = M*N+M;;

AXIOM MINUS:	∀M N. (M ≥ N ⊃ NATNUM(M-N)),
		∀M. M-0 = M,
		∀M N. (M - SUCC N = PRED(M - N));;

AXIOM GREATER:	∀M. M≥0,
		∀M. (0≥M ⊃ M=0),
		∀M N. (¬(M=0)∧¬(N=0)∧M≥N ≡ PRED M ≥ PRED N);;

AXIOM ONE:	SUCC 0 = 1;;